module myexamples/sudoku

abstract sig Num { sudoku : Num one -> one Num }
abstract sig B1, B2, B3 extends Num {}

one sig N1, N2, N3 extends B1 {}
one sig N4, N5, N6 extends B2 {}
one sig N7, N8, N9 extends B3 {}

abstract sig NumSet  { s: set Num }
one sig R1, R2 extends NumSet{}

//abstract sig R1, R2 extends Num {}

//fact rows_onto { all x: Num | Num in sudoku[x,Num] }
fact columns_onto { all y: Num | Num in sudoku[Num,y] }

fact B1B1_onto { Num in sudoku[B1,B1] }
fact B1B2_onto { Num in sudoku[B1,B2] }
fact B1B3_onto { Num in sudoku[B1,B3] }
fact B2B1_onto { Num in sudoku[B2,B1] }
fact B2B2_onto { Num in sudoku[B2,B2] }
fact B2B3_onto { Num in sudoku[B2,B3] }
fact B3B1_onto { Num in sudoku[B3,B1] }
fact B3B2_onto { Num in sudoku[B3,B2] }
fact B3B3_onto { Num in sudoku[B3,B3] }

fact fr{
R1.s = N2 + N3 + N4
R2.s = N6 + N7 + N8
}

fact test1 { Num in sudoku[R1.s,R1.s]}
fact test2 { Num in sudoku[R1.s,R2.s]}
fact test3 { Num in sudoku[R2.s,R1.s]}
fact test4 { Num in sudoku[R2.s,R2.s]}

assert rows_onto { all x: Num | Num in sudoku[x,Num] }
//check rows_onto


fact problem2{
N4->N3 in sudoku[N1]
N4->N7 +N7->N3 in sudoku[N2]
N1->N2 + N9->N8 in sudoku[N3]
N3->N6 + N6->N5 in sudoku[N4]
N2->N9 + N3->N1 + N4->N6 in sudoku[N5]
N1->N3 + N5->N7 + N6->N1 + N7->N2 in sudoku[N6]
N8->N3 + N9->N1  in sudoku[N7]
N2->N8 + N5->N4  in sudoku[N8]
N3->N2  in sudoku[N9]

}


pred show () {}
run show
